Verification¶
Up until now we’ve learned how to install Imandra, learned its basic syntax, semantics and features as a programming language but we've only briefly touched on its code analysis and verification capabilities.
Imandra extends OCaml with 5 different keywords (equivalent APIs using normal OCaml functions are also available), adding verification statements to the language:
instance <func>: this keyword takes an anonymous function representing a goal and attempts to find an instance that satisfies it. It is useful for answering the question "What is an example value that satisfies this particular property?".
In [1]:
instance (fun x -> x + x = 4)
Out[1]:
- : Z.t -> bool = <fun> module CX : sig val x : Z.t end
Instance (after 0 steps, 0.011s): let x = 2
Instance
Loading..
proof attempt
| ground_instances | 0 | ||||||||||||||
| definitions | 0 | ||||||||||||||
| inductions | 0 | ||||||||||||||
| search_time | 0.011s | ||||||||||||||
| details | Expand
|
Expand
start[0.011s] :var_0: + :var_0: = 4
simplify
into :var_0: = 2
expansions []
rewrite_steps forward_chaining - Sat (Some let x = 2 )
Loading..
verify <func>: this keyword takes an anonymous function (a lambda term) representing a goal and attempts to prove it. If the proof attempt fails, Imandra will generate aCXmodule instantiating a counterexample to the goal.
In [2]:
verify (fun x -> x + 1 > x)
Out[2]:
- : int -> bool = <fun>
Proved
proof
| ground_instances | 0 | ||||||||||||
| definitions | 0 | ||||||||||||
| inductions | 0 | ||||||||||||
| search_time | 0.010s | ||||||||||||
| details | Expand
|
Expand
start[0.010s] (:var_0: + 1) > :var_0:
simplify
into true
expansions []
rewrite_steps forward_chaining unsat
(mp (asserted (not true)) (rewrite (= (not true) false)) false)
Loading..
Loading..
theorem name = <func>: this keyword takes a name and a lambda term and installs the lambda term as a theorem (if the goal it represents can be proven) that can be reused in further proofs.
In [3]:
theorem monotonic_ints n = succ n > n
Out[3]:
val monotonic_ints : int -> bool = <fun>
Proved
proof
| ground_instances | 0 | ||||||||||||
| definitions | 0 | ||||||||||||
| inductions | 0 | ||||||||||||
| search_time | 0.011s | ||||||||||||
| details | Expand
|
Expand
start[0.011s] (:var_0: + 1) > :var_0:
simplify
into true
expansions []
rewrite_steps forward_chaining unsat
(mp (asserted (not true)) (rewrite (= (not true) false)) false)
Loading..
Loading..
lemma name = <func>: this keyword is a synonym oftheoremaxiom name = <func>: this keyword works liketheorem, but unconditionally installs the goal as a valid theorem, without trying to prove it. This keyword is extremely dangerous as it can make Imandra's internal logic inconsistent and should thus be avoided.
Moreover, several Ocaml attributes can be used on the function body to decide which technique Imandra should use to verify a goal, provide verification hints, and control how Imandra should install a particular lemma/theorem:
[@@bmc]: applies toinstance,verify,theoremandlemma, instructs Imandra to use bounded model checking on the goal instead of unrolling.
In [4]:
verify (fun _ -> true) [@@bmc] (** TODO **)
Out[4]:
- : 'a -> bool = <fun>
Proved
[@@simp]: applies toinstance,verify,theoremandlemma, instructs Imandra to apply simplification on the goal before applying unrolling.
In [5]:
verify (fun x -> x @ [] @ x = x @ x) [@@simp]
Out[5]:
- : 'a list -> bool = <fun>
Proved
proof
| ground_instances | 0 | ||||||||||||
| definitions | 1 | ||||||||||||
| inductions | 0 | ||||||||||||
| search_time | 0.030s | ||||||||||||
| details | Expand
|
Expand
start[0.030s] List.append :var_0: (List.append [] :var_0:) = List.append :var_0: :var_0:
simplify
into true
expansions List.append
rewrite_steps forward_chaining unsat
(mp (asserted (not true)) (rewrite (= (not true) false)) false)
Loading..
Loading..
[@@simplify]: synonym of[@@simp][@@induct <flag?>]: applies toinstance,verify,theoremandlemma, instructs Imandra to attempt proving the goal using induction instead of unrolling. Flag can be one of:functional <func args..>,structural <arg?>,structural_mult <arg?>,structural_add <arg?>(structuralis just a synonym forstructural_add)
In [6]:
verify (fun x y -> List.length x + List.length y = List.length (x@y)) [@@induct]
Out[6]:
- : 'a list -> 'a list -> bool = <fun> Goal: List.length x + List.length y = List.length (x @ y). 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- List.length x + List.length y = List.length (List.append x y) Verified up to bound 10 (after 0.053s). Must try induction. The recursive terms in the conjecture suggest 3 inductions. Subsumption and merging reduces this to 2. Only 1 of those schemes are unflawed. We shall induct according to a scheme derived from List.append. Induction scheme: (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x). 2 nontautological subgoals. Subgoal 1.2: H0. x = [] |--------------------------------------------------------------------------- List.length x + List.length y = List.length (List.append x y) But simplification reduces this to true, using the definitions of List.append and List.length. Subgoal 1.1: H0. not (x = []) H1. List.length (List.tl x) + List.length y = List.length (List.append (List.tl x) y) |--------------------------------------------------------------------------- List.length x + List.length y = List.length (List.append x y) But simplification reduces this to true, using the definitions of List.append and List.length.
Proved
proof
| ground_instances | 0 |
| definitions | 5 |
| inductions | 1 |
| search_time | 0.177s |
Expand
start[0.177s, "Goal"] List.length :var_0: + List.length :var_1: = List.length (List.append :var_0: :var_1:)
subproof
List.length x + List.length y = List.length (List.append x y)start[0.177s, "1"] List.length x + List.length y = List.length (List.append x y)
induction on (functional ) :scheme (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x)
Split ((not (x = []) || List.length x + List.length y = List.length (List.append x y)) && (not (not (x = []) && List.length (List.tl x) + List.length y = List.length (List.append (List.tl x) y)) || List.length x + List.length y = List.length (List.append x y)) :cases [not (x = []) || List.length x + List.length y = List.length (List.append x y); (x = [] || not (List.length (List.tl x) + List.length y = List.length (List.append (List.tl x) y))) || List.length x + List.length y = List.length (List.append x y)])subproof
(x = [] || not (List.length (List.tl x) + List.length y = List.length (List.append (List.tl x) y))) || List.length x + List.length y = List.length (List.append x y)start[0.086s, "1.1"] (x = [] || not (List.length (List.tl x) + List.length y = List.length (List.append (List.tl x) y))) || List.length x + List.length y = List.length (List.append x y)simplify
into true
expansions [List.length, List.append, List.length]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
subproof
not (x = []) || List.length x + List.length y = List.length (List.append x y)start[0.086s, "1.2"] not (x = []) || List.length x + List.length y = List.length (List.append x y)
simplify
into true
expansions [List.append, List.length]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
Loading..
[@@auto]: synonym of[@@induct], does not support flags[@@rw]: applies totheorem,lemma,axiom, instructs Imandra to install the goal as a rewrite rule (if proving succeded).
In [7]:
theorem len_append x y = List.length (x@y) = List.length x + List.length y [@@induct] [@@rw]
Out[7]:
val len_append : 'a list -> 'a list -> bool = <fun> Goal: List.length (x @ y) = List.length x + List.length y. 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- List.length (List.append x y) = List.length x + List.length y Verified up to bound 10 (after 0.051s). Must try induction. The recursive terms in the conjecture suggest 3 inductions. Subsumption and merging reduces this to 2. Only 1 of those schemes are unflawed. We shall induct according to a scheme derived from List.append. Induction scheme: (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x). 2 nontautological subgoals. Subgoal 1.2: H0. x = [] |--------------------------------------------------------------------------- List.length (List.append x y) = List.length x + List.length y But simplification reduces this to true, using the definitions of List.append and List.length. Subgoal 1.1: H0. not (x = []) H1. List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y |--------------------------------------------------------------------------- List.length (List.append x y) = List.length x + List.length y But simplification reduces this to true, using the definitions of List.append and List.length.
Proved
proof
| ground_instances | 0 |
| definitions | 5 |
| inductions | 1 |
| search_time | 0.186s |
Expand
start[0.186s, "Goal"] List.length (List.append :var_0: :var_1:) = List.length :var_0: + List.length :var_1:
subproof
List.length (List.append x y) = List.length x + List.length ystart[0.185s, "1"] List.length (List.append x y) = List.length x + List.length y
induction on (functional ) :scheme (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x)
Split ((not (x = []) || List.length (List.append x y) = List.length x + List.length y) && (not (not (x = []) && List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y) || List.length (List.append x y) = List.length x + List.length y) :cases [not (x = []) || List.length (List.append x y) = List.length x + List.length y; (x = [] || not (List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y)) || List.length (List.append x y) = List.length x + List.length y])subproof
(x = [] || not (List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y)) || List.length (List.append x y) = List.length x + List.length ystart[0.087s, "1.1"] (x = [] || not (List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y)) || List.length (List.append x y) = List.length x + List.length ysimplify
into true
expansions [List.length, List.length, List.append]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
subproof
not (x = []) || List.length (List.append x y) = List.length x + List.length ystart[0.087s, "1.2"] not (x = []) || List.length (List.append x y) = List.length x + List.length y
simplify
into true
expansions [List.length, List.append]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
List.len_nonnegative
Loading..
[@@rewrite]: synonym of[@@rw][@@fc]: applies totheorem,lemma,axiom, instructs Imandra to install the goal as a forward chaining rule (if proving succeded).
In [8]:
theorem len_non_neg x = (List.length x) [@trigger] >= 0 [@@simp] [@@fc]
Out[8]:
val len_non_neg : 'a list -> bool = <fun>
Proved
proof
| ground_instances | 0 | ||||||||||||
| definitions | 0 | ||||||||||||
| inductions | 0 | ||||||||||||
| search_time | 0.039s | ||||||||||||
| details | Expand
|
Expand
start[0.039s] List.length :var_0: >= 0
simplify
into true
expansions []
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
unsat
(mp (asserted (not true)) (rewrite (= (not true) false)) false)
Loading..
Loading..
[@@forward_chaining]: synonym of[@@fc][@@apply <thm args..>]: applies toinstance,theorem,lemma,verify, instructs Imandra to instantiatethmwithargsand add its instantiation to the context (the set of hypotheses) of the current goal (i.e. given a goalg, it instructs imandra to solvethm args.. ==> gin order to proveg, where==>is theimplyoperator.)
[@@disable <f>]: applies toinstance,theorem,lemma,verify, when used in the context of solving via[@@induct]. Iffis a rule (rewrite or forward chaining) hints Imandra to ignore it while solving the goal, iffis a function hints Imandra to leave the function definition uninterpreted. Imandra might chose to ignore this hint if ignoring it leads to immediate closure of the goal.
In [10]:
verify (fun x -> x @ [] = x) [@@auto] [@@disable List.append_to_nil]
Out[10]:
- : 'a list -> bool = <fun> Goal: x @ [] = x. 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- List.append x [] = x But simplification reduces this to true, using the rewrite rule List.append_to_nil.
Proved
[@@enable <f>]applies toinstance,theorem,lemma,verify, when used in the context of solving via[@@induct]. Iffis a rule (rewrite or forward chaining) instructs Imandra to consider it while solving the goal, iffis a function instructs Imandra to interpret the function definition.
In [11]:
#disable List.append_to_nil;;
verify (fun x -> x @ [] = x) [@@auto] [@@enable List.append_to_nil];;
#enable List.append_to_nil;;
Out[11]:
- : 'a list -> bool = <fun> Goal: x @ [] = x. 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- List.append x [] = x Verified up to bound 10 (after 0.054s). Must try induction. We shall induct according to a scheme derived from List.append. Induction scheme: (x = [] ==> φ x) && (not (x = []) && φ (List.tl x) ==> φ x). 2 nontautological subgoals. Subgoal 1.2: H0. x = [] |--------------------------------------------------------------------------- List.append x [] = x But simplification reduces this to true, using the definition of List.append. Subgoal 1.1: H0. not (x = []) H1. List.append (List.tl x) [] = List.tl x |--------------------------------------------------------------------------- List.append x [] = x But simplification reduces this to true, using the definition of List.append.
Proved
proof
| ground_instances | 0 |
| definitions | 2 |
| inductions | 1 |
| search_time | 0.097s |
Expand
start[0.097s, "Goal"] List.append :var_0: [] = :var_0:
subproof
List.append x [] = xstart[0.097s, "1"] List.append x [] = x
induction on (functional ) :scheme (x = [] ==> φ x) && (not (x = []) && φ (List.tl x) ==> φ x)
Split ((not (x = []) || List.append x [] = x) && (not (not (x = []) && List.append (List.tl x) [] = List.tl x) || List.append x [] = x) :cases [not (x = []) || List.append x [] = x; (x = [] || not (List.append (List.tl x) [] = List.tl x)) || List.append x [] = x])subproof
(x = [] || not (List.append (List.tl x) [] = List.tl x)) || List.append x [] = xstart[0.028s, "1.1"] (x = [] || not (List.append (List.tl x) [] = List.tl x)) || List.append x [] = x
simplify
into true
expansions List.append
rewrite_steps forward_chaining
subproof
not (x = []) || List.append x [] = xstart[0.028s, "1.2"] not (x = []) || List.append x [] = x
simplify
into true
expansions List.append
rewrite_steps forward_chaining
Loading..
Now that we've learned the syntax of Imandra's verification statements, let's learn how we can use them to:
verify the absence of bugs
generate counterexamples and test cases
prove the validity of properties.
Bounded Solving¶
TODO: move the more general stuff about BMC from unrolling here.
Unrolling¶
The first tool that Imandra makes available in our verification toolbox is unrolling, a form of bounded model checking (BMC) backed by satisfiability solving (SMT).
Since BMC is a completely automated technique, requiring no user intervention in order to terminate, we don't need to understand any complex theories or techniques in order to start using it and reaping its benefits.
In order to start using unrolling for verification or instance search, we simply use the appropriate statement without an alternative method annotation.
Let's use unrolling to find an instance of two lists of integers, whose sum equals to the length of the two lists concatenated. We shall constrain the total length of the two lists to be at least 10, otherwise Imandra will "cheat" and find two empty lists as first solution:
In [12]:
instance
(fun x y ->
List.length (x@y) > 10
&& List.fold_left (+) 0 (x@y) = List.length (x@y))
Out[12]:
- : Z.t list -> Z.t list -> bool = <fun> module CX : sig val x : Z.t list val y : Z.t list end
Instance (after 31 steps, 0.136s): let x = [7854] let y = [38; (-8882); 8365; (-1); 0; 974; (-3099); 2455; (-3343); (-4350)]
Instance
Loading..
proof attempt
| ground_instances | 31 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| definitions | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| inductions | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| search_time | 0.136s | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| details | Expand
|
Expand
start[0.136s] List.length (List.append :var_0: :var_1:) > 10 && List.fold_left + 0 (List.append :var_0: :var_1:) = List.length (List.append :var_0: :var_1:)simplify
into not (List.length (List.append :var_0: :var_1:) <= 10) && List.fold_left + 0 (List.append :var_0: :var_1:) = List.length (List.append :var_0: :var_1:)
expansions []
rewrite_steps forward_chaining - unroll
expr (|\|`List.fold_left +[0]`_2583\|| 0 (|\|List.append_2575\|| x_2567 y_2568))
expansions - unroll
expr (|\|List.append_2575\|| x_2567 y_2568)
expansions - unroll
expr (|\|List.length_2580\|| (|\|List.append_2575\|| x_2567 y_2568))
expansions - unroll
expr (|\|`List.fold_left +[0]`_2583\|| (+ 0 (|\|get.::.0_2573\|| (|\|List.append_2575\|| x_2567 y_2568)…
expansions - unroll
expr (|\|List.append_2575\|| (|\|get.::.1_2574\|| x_2567) y_2568)
expansions - unroll
expr (|\|List.length_2580\|| (|\|get.::.1_2574\|| (|\|List.append_2575\|| x_2567 y_2568)))
expansions - unroll
expr (let ((a!1 (+ 0 (|\|get.::.0_2573\|| (|\|List.append_2575\|| x_2567 y_2568)) …expansions - unroll
expr (|\|List.length_2580\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|| (|\|List.append_2575\|| x_25…expansions - unroll
expr (let ((a!1 (|\|get.::.0_2573\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (|\|List.append_2575\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|| x_2567)) y_2568)
expansions - unroll
expr (let ((a!1 (|\|get.::.1_2574\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.1_2574\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.0_2573\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.1_2574\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (|\|List.append_2575\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|| x_2567))) …
expansions - unroll
expr (let ((a!1 (|\|get.::.0_2573\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.1_2574\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.0_2573\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.0_2573\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.1_2574\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.1_2574\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.0_2573\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.1_2574\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.0_2573\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.1_2574\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.1_2574\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.0_2573\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.1_2574\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.0_2573\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.1_2574\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - unroll
expr (let ((a!1 (|\|get.::.1_2574\|| (|\|get.::.1_2574\|| (|\|get.::.1_2574\|…expansions - Sat (Some let x = [7854] let y = [38; (-8882); 8365; (-1); 0; 974; (-3099); 2455; (-3343); (-4350)] )
Loading..
Imandra was able to find a solution instantly, and reflected it into our runtime in the CX module. Let's use that to compute and make sure that Imandra is indeed correct:
In [13]:
List.length (CX.x@CX.y);;
List.fold_left (+) 0 (CX.x@CX.y);;
Out[13]:
- : Z.t = 11 - : Z.t = 11
This verification technique - albeit simpler and weaker than the more advanced techniques we'll discuss later on - is often enough for most practical problems and thus is the default "mode" of verification that Imandra uses for both verification and instance search.
Unrolling works by creating a call graph for the negation of the goal we've asked Imandra to verify, and by recursively extending this graph by expanding each function call into its definition, up to depth k (hence bounded), checking at each step for satisfiability.
If at any step of the unrolling process, the negation of our original goal is satisfiable, then it means that Imandra has found a counterexample for our original goal, which is then considered falsified.
If, on the other hand, Imandra couldn't find a counterexample, then if unrolling stopped before depth k, it means that our original goal is indeed a theorem valid for all possible inputs, otherwise if Imandra stopped unrolling at depth k but more unrolling is possible, that gives us the weaker result of a guarantee that our goal is valid up to depth k.
The depth k of unrolling defaults to 100 and can be controlled using the #unroll <n> command.
Let's try to understand in practice how k plays into unrolling. Given this simple function that recursively decreases an integer until it reaches 0, then returns 1:
In [14]:
let rec f x =
if x <= 0 then
1
else
f (x - 1)
Out[14]:
val f : int -> Z.t = <fun>
termination proof
Termination proof
call `f (x - 1)` from `f x`
| original | f x | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | f (x - 1) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (if x >= 0 then x else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (if (x - 1) >= 0 then x - 1 else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [not (x <= 0)] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
Let's verify that up to x < 100, every input causes the function to return 1:
In [15]:
verify (fun x -> x < 100 ==> f x = 1)
Out[15]:
- : int -> bool = <fun>
Proved
proof
| ground_instances | 100 | ||||||||||||||||||||||||||||||||
| definitions | 0 | ||||||||||||||||||||||||||||||||
| inductions | 0 | ||||||||||||||||||||||||||||||||
| search_time | 0.501s | ||||||||||||||||||||||||||||||||
| details | Expand
|
Expand
start[0.501s] :var_0: < 100 ==> f :var_0: = 1
simplify
into 100 <= :var_0: || f :var_0: = 1
expansions []
rewrite_steps forward_chaining - unroll
expr (f_2600 x_2613)
expansions - unroll
expr (f_2600 (+ (- 1) x_2613))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) x_2613))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) x_2613))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) x_2613))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) x_2613))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2613))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2613))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2613))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2613))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2613))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions unsat
(let ((a!1 (= (ite (<= x_2613 99) 1 (f_2600 (+ (- 100) x_2613))) 1)) (a!3 (monotonicity (rewri…
Loading..
Loading..
But watch what happens if we ask Imandra to verify this for x < 101, thus exceding the number of recursive calls that Imandra unrolls by default:
In [16]:
verify (fun x -> x < 101 ==> f x = 1)
Out[16]:
- : int -> bool = <fun>
Unknown (Verified up to bound 100)
Expand
| expanded |
|
| blocked |
|
Loading..
proof attempt
| ground_instances | 101 |
| definitions | 0 |
| inductions | 0 |
| search_time | 0.554s |
Expand
start[0.554s] :var_0: < 101 ==> f :var_0: = 1
simplify
into 101 <= :var_0: || f :var_0: = 1
expansions []
rewrite_steps forward_chaining - unroll
expr (f_2600 x_2622)
expansions - unroll
expr (f_2600 (+ (- 1) x_2622))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) x_2622))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) x_2622))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) x_2622))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) x_2622))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2622))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2622))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2622))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2622))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2622))
expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions - unroll
expr (f_2600 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1…expansions
Loading..
As expected, since the recursion depth needed to prove this exceeds the unrolling depth we set, Imandra could only prove this property up to bound k. This is in fact a property that is better suited for verification by induction, which we'll touch on later, but served as a perfect illustration of how k affects Imandra's unrolling.
It's important to stress that while unrolling is mostly suited for verifying finite-state properties, for most practical problems its bounded verification gives immediate results that are valuable long before needing to reach for more complex verification tools.
Blast¶
TODO: BAT-BMC
Simplification¶
Imandra comes with a powerful symbolic simplifier and partial evaluator which is used transparently when proving by induction, but can also be used separately to simplify the goal before reaching for unrolling.
Simplification is not a verification technique per se, but in some cases it can lead to a goal that is trivially true (a tautology) or false allowing the verification process to terminate before unrolling or induction are even brought to the table.
As the name suggests, simplification is a process that attempts to "simplify" a logical formula as much as possible. It does so by looping over the formula eliminating unreachable branches, partially evaluating it as much as possible doing symbolic evaluation and by applying all the available rewrite or forward chaining rules that match the current goal.
Notably, because the symbolic evaluation semantics of the simplifier operate on a compact digraph representation of the underlying call tree, simplification can be thought as having memoized semantics for free.
We can see an example of this by using the following naive recursive version of the fibonacci function:
In [17]:
let rec fib n =
if n <= 1 then
1
else
(fib (n-1)) + (fib (n-2))
Out[17]:
val fib : int -> Z.t = <fun>
termination proof
Termination proof
call `fib (n - 1)` from `fib n`
| original | fib n | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | fib (n - 1) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (if n >= 0 then n else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [not (n <= 1)] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
call `fib (n - 2)` from `fib n`
| original | fib n | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | fib (n - 2) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (if n >= 0 then n else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (if (n - 2) >= 0 then n - 2 else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [not (n <= 1)] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
If we try to use Imandra's simplification to search for a solution for fib 200, Imandra comes back to us with a solution immediately:
In [18]:
#check_models false;;
instance (fun x -> x = fib 200) [@@simp];;
#check_models true;;
Out[18]:
- : Z.t -> bool = <fun> module CX : sig val x : Z.t end
Instance (after 0 steps, 0.047s): let x = 453973694165307953197296969697410619233826
Instance
Loading..
proof attempt
| ground_instances | 0 | ||||||||||||||
| definitions | 201 | ||||||||||||||
| inductions | 0 | ||||||||||||||
| search_time | 0.047s | ||||||||||||||
| details | Expand
|
Expand
start[0.047s] :var_0: = fib 200
simplify
into x = 453973694165307953197296969697410619233826
expansions [fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib]
rewrite_steps forward_chaining - Sat (Some let x = 453973694165307953197296969697410619233826 )
Loading..
If, however, we tried to use normal evaluation to compute fib 200, OCaml would take over 10 minutes in order to come back with a response (the #check_models false command here is used to tell Imandra not to validate the instance found against OCaml, as that requires the expensive computation of fib 200)
Now that we know what simplification does, let's learn about how to influence it using rewrite and forward chaining rules.
Rewrite Rule¶
A rewrite rule is a theorem of the form ctx ==> lhs = rhs which Imandra can use in further proofs to replace terms that match with lhs with the appropriate instantiation of rhs in the current goal, provided that the instantiation of ctx holds.
With a concrete example, given the rewrite rule rev_len, proving that the length of a list is equal to the length of the list reversed (notice that Imandra uses a previously defined rewrite rule in order to prove this rewrite rule!):
In [19]:
lemma rev_len x =
List.length (List.rev x) = List.length x
[@@auto] [@@rw]
Out[19]:
val rev_len : 'a list -> bool = <fun> Goal: List.length (List.rev x) = List.length x. 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- List.length (List.rev x) = List.length x Verified up to bound 10 (after 0.052s). Must try induction. The recursive terms in the conjecture suggest 2 inductions. Subsumption and merging reduces this to 1. We shall induct according to a scheme derived from List.length. Induction scheme: (x = [] ==> φ x) && (not (x = []) && φ (List.tl x) ==> φ x). 2 nontautological subgoals. Subgoal 1.2: H0. x = [] |--------------------------------------------------------------------------- List.length (List.rev x) = List.length x But simplification reduces this to true, using the definitions of List.length and List.rev. Subgoal 1.1: H0. not (x = []) H1. List.length (List.rev (List.tl x)) = List.length (List.tl x) |--------------------------------------------------------------------------- List.length (List.rev x) = List.length x This simplifies, using the definitions of List.length and List.rev to: Subgoal 1.1': H0. List.length (List.rev (List.tl x)) = List.length (List.tl x) H1. x <> [] |--------------------------------------------------------------------------- List.length (List.append (List.rev (List.tl x)) ((List.hd x) :: [])) = 1 + List.length (List.tl x) But simplification reduces this to true, using the definition of List.length, and the rewrite rule len_append.
Proved
proof
| ground_instances | 0 |
| definitions | 7 |
| inductions | 1 |
| search_time | 0.368s |
Expand
start[0.368s, "Goal"] List.length (List.rev :var_0:) = List.length :var_0:
subproof
List.length (List.rev x) = List.length xstart[0.368s, "1"] List.length (List.rev x) = List.length x
induction on (functional ) :scheme (x = [] ==> φ x) && (not (x = []) && φ (List.tl x) ==> φ x)
Split ((not (x = []) || List.length (List.rev x) = List.length x) && (not (not (x = []) && List.length (List.rev (List.tl x)) = List.length (List.tl x)) || List.length (List.rev x) = List.length x) :cases [not (x = []) || List.length (List.rev x) = List.length x; (x = [] || not (List.length (List.rev (List.tl x)) = List.length (List.tl x))) || List.length (List.rev x) = List.length x])subproof
(x = [] || not (List.length (List.rev (List.tl x)) = List.length (List.tl x))) || List.length (List.rev x) = List.length xstart[0.275s, "1.1"] (x = [] || not (List.length (List.rev (List.tl x)) = List.length (List.tl x))) || List.length (List.rev x) = List.length x
simplify
into (List.length (List.append (List.rev (List.tl x)) ((List.hd x) :: [])) = 1 + List.length (List.tl x) || not (List.length (List.rev (List.tl x)) = List.length (List.tl x))) || x = []
expansions [List.length, List.rev]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
simplify
into true
expansions [List.length, List.length]
rewrite_steps len_append
forward_chaining List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
subproof
not (x = []) || List.length (List.rev x) = List.length xstart[0.275s, "1.2"] not (x = []) || List.length (List.rev x) = List.length x
simplify
into true
expansions [List.length, List.length, List.rev]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
Loading..
Every time Imandra will now encounter, during a proof, a term of the form List.length (List.rev lst) it will replace it with the simpler form List.length lst (lst can be an arbitrary term).
Both ctx and rhs can be omitted, in which case Imandra will default them to true (i.e. ctx ==> lhs is equal to ctx ==> lhs = true and lhs = rhs is equal to true ==> lhs = rhs).
Imandra's rewriting is:
unconditional: if a rewrite rule is found that applies to the current goal, it will be applied no matter what. This means that adding two rewrite rules, one of the form
a = band one of the formb = a, will cause Imandra to run into an infinite loop replacingaforb, thenbforaand so onoriented: given a rule of the form
a = b, Imandra will only peform the substitution left to right, never right to left in order to avoid loops
For those reasons, when adding a new rewrite rule, users should be very careful to orient the equality so that rhs is always simpler or more normalised than lhs. If it's not clear what it means for a lhs to be "better" than its rhs equivalent, e.g. in the case of the proof for the associativity of list concatenation x @ (y @ z) = (x @ y) @ z, a canonical form should be chosen (e.g. rewriting from right associative to left associative in this case) and kept in mind for further rules.
In order for a theorem to be a valid rewrite rule, the lhs must contain all the free variables of the theorem (i.e. the arguments to the lambda term representing the goal). There is an exception to this rule: if the lhs does not contain all the free variables of the theorem but the ctx has a term containing the remaining free variables, it can be annotated with [@trigger rw], signaling Imandra that the contextual term will be used to complete the matching.
It can be hard to understand when or why this would be useful, as usual an example will clarify things: let's first define a subset function on lists:
In [20]:
let rec subset x y =
match x with
| [] -> true
| x :: xs ->
if List.mem x y then subset xs y
else false
Out[20]:
val subset : 'a list -> 'a list -> bool = <fun>
termination proof
Termination proof
call `subset (List.tl x) y` from `subset x y`
| original | subset x y | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | subset (List.tl x) y | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (Ordinal.count x) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (Ordinal.count (List.tl x)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [List.mem (List.hd x) y && not (x = [])] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
Let's now suppose that we want to verify the transitivity of subset:
In [21]:
#max_induct 1;;
verify (fun x y z -> subset x y && subset y z ==> subset x z) [@@auto]
Out[21]:
- : 'a list -> 'a list -> 'a list -> bool = <fun> Goal: subset x y && subset y z ==> subset x z. 1 nontautological subgoal. Subgoal 1: H0. subset x y H1. subset y z |--------------------------------------------------------------------------- subset x z Verified up to bound 10 (after 0.052s). Must try induction. The recursive terms in the conjecture suggest 3 inductions. Subsumption and merging reduces this to 2. Only 1 of those schemes are unflawed. We shall induct according to a scheme derived from subset. Induction scheme: (not (List.mem (List.hd x) y && not (x = [])) ==> φ z y x) && (not (x = []) && List.mem (List.hd x) y && φ z y (List.tl x) ==> φ z y x). 2 nontautological subgoals. Subgoal 1.2: H0. subset x y H1. subset y z |--------------------------------------------------------------------------- C0. List.mem (List.hd x) y && not (x = []) C1. subset x z This simplifies, using the definition of subset to: Subgoal 1.2': H0. subset y z H1. subset x y |--------------------------------------------------------------------------- C0. subset x z C1. List.mem (List.hd x) y But simplification reduces this to true, using the definition of subset. Subgoal 1.1: H0. not (x = []) H1. List.mem (List.hd x) y H2. subset (List.tl x) y && subset y z ==> subset (List.tl x) z H3. subset x y H4. subset y z |--------------------------------------------------------------------------- subset x z This simplifies, using the definition of subset to: Subgoal 1.1': H0. subset y z H1. subset (List.tl x) z H2. subset (List.tl x) y H3. List.mem (List.hd x) y H4. x <> [] |--------------------------------------------------------------------------- List.mem (List.hd x) z Verified up to bound 10 (after 0.052s). We can eliminate destructors by the following substitution: x -> x1 :: x2 This produces the modified subgoal: Subgoal 1.1'': H0. subset y z H1. subset x2 z H2. subset x2 y H3. List.mem x1 y |--------------------------------------------------------------------------- List.mem x1 z Verified up to bound 10 (after 0.053s). Must try induction. Checkpoints: H0. subset y z H1. subset x2 z H2. subset x2 y H3. List.mem x1 y |--------------------------------------------------------------------------- List.mem x1 z Error: Maximum induction depth reached (1). You can set this with #max_induct.
It looks like Imandra needs an additional lemma in order to prove this, by inspecting the checkpoint it looks like all we need is a rule relating subset with List.mem, let's attempt to define it:
In [22]:
lemma mem_subset x y z =
List.mem x y && subset y z ==> List.mem x z
[@@induct] [@@rewrite]
Out[22]:
val mem_subset : 'a -> 'a list -> 'a list -> bool = <fun> Goal: List.mem x y && subset y z ==> List.mem x z. 1 nontautological subgoal. Subgoal 1: H0. List.mem x y H1. subset y z |--------------------------------------------------------------------------- List.mem x z Verified up to bound 10 (after 0.052s). Must try induction. The recursive terms in the conjecture suggest 3 inductions. Subsumption and merging reduces this to 2. However, scheme scoring gives us a clear winner. We shall induct according to a scheme derived from List.mem. Induction scheme: (y = [] ==> φ z y x) && (not (y = []) && φ z (List.tl y) x ==> φ z y x). 2 nontautological subgoals. Subgoal 1.2: H0. y = [] H1. List.mem x y H2. subset y z |--------------------------------------------------------------------------- List.mem x z But simplification reduces this to true, using the definition of List.mem. Subgoal 1.1: H0. not (y = []) H1. List.mem x (List.tl y) && subset (List.tl y) z ==> List.mem x z H2. List.mem x y H3. subset y z |--------------------------------------------------------------------------- List.mem x z But simplification reduces this to true, using the definitions of List.mem and subset. File "jupyter cell 22", line 1, characters 6-93: Error: in rewrite rule, variable (y : 'a list) does not occur in left-hand side of the rule or in `[@trigger rw]` terms
Proved
proof
| ground_instances | 0 |
| definitions | 5 |
| inductions | 1 |
| search_time | 0.383s |
Expand
start[0.383s, "Goal"] List.mem :var_0: :var_1: && subset :var_1: :var_2: ==> List.mem :var_0: :var_2:
subproof
(not (List.mem x y) || not (subset y z)) || List.mem x zstart[0.383s, "1"] (not (List.mem x y) || not (subset y z)) || List.mem x z
induction on (functional ) :scheme (y = [] ==> φ z y x) && (not (y = []) && φ z (List.tl y) x ==> φ z y x)Split ((((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x z) && (((not (not (y = []) && ((not (List.mem x (List.tl y)) || not (subset (List.tl y) z)) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x z) :cases [((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x z; (((y = [] || not (not (List.mem x (List.tl y) && subset (List.tl y) z) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x z])subproof
(((y = [] || not (not (List.mem x (List.tl y) && subset (List.tl y) z) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x zstart[0.210s, "1.1"] (((y = [] || not (not (List.mem x (List.tl y) && subset (List.tl y) z) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x zsimplify
into true
expansions [subset, List.mem, subset, List.mem]
rewrite_steps forward_chaining
subproof
((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x zstart[0.210s, "1.2"] ((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x z
simplify
into true
expansions List.mem
rewrite_steps forward_chaining
Loading..
As we can see, while Imandra was successful in proving this lemma, it failed while trying to turn this lemma into a rewrite rule, correctly suggesting us that the free variable y does not appear in the lhs term, List.mem x z. If we, however, annotate the subset y z term in the ctx with the appropriate trigger, Imandra can then successfully turn this term into a valid rewrite rule:
In [23]:
lemma mem_subset x y z =
List.mem x y && (subset y z [@trigger rw]) ==> List.mem x z
[@@induct] [@@rewrite]
Out[23]:
val mem_subset : 'a -> 'a list -> 'a list -> bool = <fun> Goal: List.mem x y && subset y z ==> List.mem x z. 1 nontautological subgoal. Subgoal 1: H0. List.mem x y H1. subset y z |--------------------------------------------------------------------------- List.mem x z Verified up to bound 10 (after 0.053s). Must try induction. The recursive terms in the conjecture suggest 3 inductions. Subsumption and merging reduces this to 2. However, scheme scoring gives us a clear winner. We shall induct according to a scheme derived from List.mem. Induction scheme: (y = [] ==> φ z y x) && (not (y = []) && φ z (List.tl y) x ==> φ z y x). 2 nontautological subgoals. Subgoal 1.2: H0. y = [] H1. List.mem x y H2. subset y z |--------------------------------------------------------------------------- List.mem x z But simplification reduces this to true, using the definition of List.mem. Subgoal 1.1: H0. not (y = []) H1. List.mem x (List.tl y) && subset (List.tl y) z ==> List.mem x z H2. List.mem x y H3. subset y z |--------------------------------------------------------------------------- List.mem x z But simplification reduces this to true, using the definitions of List.mem and subset.
Proved
proof
| ground_instances | 0 |
| definitions | 5 |
| inductions | 1 |
| search_time | 0.386s |
Expand
start[0.386s, "Goal"] List.mem :var_0: :var_1: && subset :var_1: :var_2: ==> List.mem :var_0: :var_2:
subproof
(not (List.mem x y) || not (subset y z)) || List.mem x zstart[0.386s, "1"] (not (List.mem x y) || not (subset y z)) || List.mem x z
induction on (functional ) :scheme (y = [] ==> φ z y x) && (not (y = []) && φ z (List.tl y) x ==> φ z y x)Split ((((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x z) && (((not (not (y = []) && ((not (List.mem x (List.tl y)) || not (subset (List.tl y) z)) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x z) :cases [((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x z; (((y = [] || not (not (List.mem x (List.tl y) && subset (List.tl y) z) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x z])subproof
(((y = [] || not (not (List.mem x (List.tl y) && subset (List.tl y) z) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x zstart[0.214s, "1.1"] (((y = [] || not (not (List.mem x (List.tl y) && subset (List.tl y) z) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x zsimplify
into true
expansions [subset, List.mem, subset, List.mem]
rewrite_steps forward_chaining
subproof
((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x zstart[0.214s, "1.2"] ((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x z
simplify
into true
expansions List.mem
rewrite_steps forward_chaining
Loading..
And finally, let's verify that the rewrite rule can indeed match as we expect:
In [24]:
verify (fun x y z -> subset x y && subset y z ==> subset x z) [@@auto]
Out[24]:
- : 'a list -> 'a list -> 'a list -> bool = <fun> Goal: subset x y && subset y z ==> subset x z. 1 nontautological subgoal. Subgoal 1: H0. subset x y H1. subset y z |--------------------------------------------------------------------------- subset x z Verified up to bound 10 (after 0.052s). Must try induction. The recursive terms in the conjecture suggest 3 inductions. Subsumption and merging reduces this to 2. Only 1 of those schemes are unflawed. We shall induct according to a scheme derived from subset. Induction scheme: (not (List.mem (List.hd x) y && not (x = [])) ==> φ z y x) && (not (x = []) && List.mem (List.hd x) y && φ z y (List.tl x) ==> φ z y x). 2 nontautological subgoals. Subgoal 1.2: H0. subset x y H1. subset y z |--------------------------------------------------------------------------- C0. List.mem (List.hd x) y && not (x = []) C1. subset x z This simplifies, using the definitions of List.mem and subset, and the rewrite rule mem_subset to: Subgoal 1.2': H0. subset y z H1. subset x y |--------------------------------------------------------------------------- C0. subset x z C1. List.mem (List.hd x) y But simplification reduces this to true, using the definition of subset. Subgoal 1.1: H0. not (x = []) H1. List.mem (List.hd x) y H2. subset (List.tl x) y && subset y z ==> subset (List.tl x) z H3. subset x y H4. subset y z |--------------------------------------------------------------------------- subset x z But simplification reduces this to true, using the definitions of List.mem and subset, and the rewrite rule mem_subset.
Proved
proof
| ground_instances | 0 |
| definitions | 9 |
| inductions | 1 |
| search_time | 1.552s |
Expand
start[1.552s, "Goal"] subset :var_0: :var_1: && subset :var_1: :var_2: ==> subset :var_0: :var_2:
subproof
(not (subset x y) || not (subset y z)) || subset x zstart[1.552s, "1"] (not (subset x y) || not (subset y z)) || subset x z
induction on (functional ) :scheme (not (List.mem (List.hd x) y && not (x = [])) ==> φ z y x) && (not (x = []) && List.mem (List.hd x) y && φ z y (List.tl x) ==> φ z y x)Split ((((List.mem (List.hd x) y && not (x = []) || not (subset x y)) || not (subset y z)) || subset x z) && (((not ((not (x = []) && List.mem (List.hd x) y) && ((not (subset (List.tl x) y) || not (subset y z)) || subset (List.tl x) z)) || not (subset x y)) || not (subset y z)) || subset x z) :cases [((not (subset x y) || not (subset y z)) || List.mem (List.hd x) y && not (x = [])) || subset x z; ((((x = [] || not (List.mem (List.hd x) y)) || not (not (subset (List.tl x) y && subset y z) || subset (List.tl x) z)) || not (subset x y)) || not (subset y z)) || subset x z])subproof
((((x = [] || not (List.mem (List.hd x) y)) || not (not (subset (List.tl x) y && subset y z) || subset (List.tl x) z)) || not (subset x y)) || not (subset y z)) || subset x zstart[1.258s, "1.1"] ((((x = [] || not (List.mem (List.hd x) y)) || not (not (subset (List.tl x) y && subset y z) || subset (List.tl x) z)) || not (subset x y)) || not (subset y z)) || subset x zsimplify
into true
expansions [subset, subset, subset, List.mem]
rewrite_steps mem_subset
mem_subset
forward_chaining
subproof
((not (subset x y) || not (subset y z)) || List.mem (List.hd x) y && not (x = [])) || subset x zstart[1.258s, "1.2"] ((not (subset x y) || not (subset y z)) || List.mem (List.hd x) y && not (x = [])) || subset x z
simplify
into ((subset x z || List.mem (List.hd x) y) || not (subset y z)) || not (subset x y)
expansions [subset, List.mem, List.mem]
rewrite_steps mem_subset
forward_chaining simplify
into true
expansions [subset, subset]
rewrite_steps forward_chaining
Loading..
Forward Chaining¶
Forward chaining is the second type of rule that Imandra allows us to register and participate in simplification.
A forward chaining rule is a theorem of the form F containing a trigger term t which must include all the free variables of the theorem. If imandra can match t with some term in the goal it's currently trying to prove, then an instantiation of F is added to the context.
With a concrete example, given the forward chaining rule len_pos, proving that the length of a list is never negative:
In [25]:
lemma len_nonnegative x =
List.length x [@trigger] >= 0
[@@simp] [@@fc]
Out[25]:
val len_nonnegative : 'a list -> bool = <fun>
Proved
proof
| ground_instances | 0 | ||||||||||||
| definitions | 0 | ||||||||||||
| inductions | 0 | ||||||||||||
| search_time | 0.040s | ||||||||||||
| details | Expand
|
Expand
start[0.040s] List.length :var_0: >= 0
simplify
into true
expansions []
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
unsat
(mp (asserted (not true)) (rewrite (= (not true) false)) false)
Loading..
Loading..
Every time Imandra will now encounter, during a proof, a term of the form List.length lst, the axiom List.length lst >= 0 will be added to the context of the goal it's trying to solve. In other words, a forward chaining rule allows Imandra to extend the database of logical facts it knows about a certain goal.
A forward chaining rule can contain multiple disjoint triggers, in that case if either of the triggers matches, the forward chaining rule applies. For example the following forward chaining version of the rev_len rewrite rule we added above, will fire if either List.length x or List.length (List.rev x) matches.
In [26]:
lemma rev_len_fc x =
List.length x [@trigger] = List.length (List.rev x) [@trigger]
[@@simp] [@@fc]
Out[26]:
val rev_len_fc : 'a list -> bool = <fun>
Proved
proof
| ground_instances | 0 | ||||||||||||
| definitions | 0 | ||||||||||||
| inductions | 0 | ||||||||||||
| search_time | 0.063s | ||||||||||||
| details | Expand
|
Expand
start[0.063s] List.length :var_0: = List.length (List.rev :var_0:)
simplify
into true
expansions []
rewrite_steps rev_len
forward_chaining List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
unsat
(mp (asserted (not true)) (rewrite (= (not true) false)) false)
Loading..
Loading..
Additionally, a forward chaining rule can also contain multiple conjoined triggers, forming a trigger cluster, in that case all the triggers must match in order for the forward chaining rule to apply.
To create a trigger cluster multiple terms must be annotated with [@trigger <x>n], where <x> is a numeric identifier common to all the triggers in the cluster. For example:
In [27]:
theorem subset_trans l1 l2 l3 =
subset l2 l3 && (subset l1 l2 [@trigger 0n])
==>
(subset l1 l3 [@trigger 0n])
[@@induct] [@@forward_chaining]
Out[27]:
val subset_trans : 'a list -> 'a list -> 'a list -> bool = <fun> Goal: subset l2 l3 && subset l1 l2 ==> subset l1 l3. 1 nontautological subgoal. Subgoal 1: H0. subset l2 l3 H1. subset l1 l2 |--------------------------------------------------------------------------- subset l1 l3 Verified up to bound 10 (after 0.052s). Must try induction. The recursive terms in the conjecture suggest 3 inductions. Subsumption and merging reduces this to 2. Only 1 of those schemes are unflawed. We shall induct according to a scheme derived from subset. Induction scheme: (not (List.mem (List.hd l1) l2 && not (l1 = [])) ==> φ l3 l2 l1) && (not (l1 = []) && List.mem (List.hd l1) l2 && φ l3 l2 (List.tl l1) ==> φ l3 l2 l1). 2 nontautological subgoals. Subgoal 1.2: H0. subset l2 l3 H1. subset l1 l2 |--------------------------------------------------------------------------- C0. List.mem (List.hd l1) l2 && not (l1 = []) C1. subset l1 l3 This simplifies, using the definitions of List.mem and subset, and the rewrite rule mem_subset to: Subgoal 1.2': H0. subset l1 l2 H1. subset l2 l3 |--------------------------------------------------------------------------- C0. subset l1 l3 C1. List.mem (List.hd l1) l2 But simplification reduces this to true, using the definition of subset. Subgoal 1.1: H0. not (l1 = []) H1. List.mem (List.hd l1) l2 H2. subset l2 l3 && subset (List.tl l1) l2 ==> subset (List.tl l1) l3 H3. subset l2 l3 H4. subset l1 l2 |--------------------------------------------------------------------------- subset l1 l3 But simplification reduces this to true, using the definitions of List.mem and subset, and the rewrite rule mem_subset.
Proved
proof
| ground_instances | 0 |
| definitions | 9 |
| inductions | 1 |
| search_time | 1.610s |
Expand
start[1.610s, "Goal"] subset :var_0: :var_1: && subset :var_2: :var_0: ==> subset :var_2: :var_1:
subproof
(not (subset l2 l3) || not (subset l1 l2)) || subset l1 l3start[1.610s, "1"] (not (subset l2 l3) || not (subset l1 l2)) || subset l1 l3
induction on (functional ) :scheme (not (List.mem (List.hd l1) l2 && not (l1 = [])) ==> φ l3 l2 l1) && (not (l1 = []) && List.mem (List.hd l1) l2 && φ l3 l2 (List.tl l1) ==> φ l3 l2 l1)Split ((((List.mem (List.hd l1) l2 && not (l1 = []) || not (subset l2 l3)) || not (subset l1 l2)) || subset l1 l3) && (((not ((not (l1 = []) && List.mem (List.hd l1) l2) && ((not (subset l2 l3) || not (subset (List.tl l1) l2)) || subset (List.tl l1) l3)) || not (subset l2 l3)) || not (subset l1 l2)) || subset l1 l3) :cases [((not (subset l2 l3) || not (subset l1 l2)) || List.mem (List.hd l1) l2 && not (l1 = [])) || subset l1 l3; ((((l1 = [] || not (List.mem (List.hd l1) l2)) || not (not (subset l2 l3 && subset (List.tl l1) l2) || subset (List.tl l1) l3)) || not (subset l2 l3)) || not (subset l1 l2)) || subset l1 l3])subproof
((((l1 = [] || not (List.mem (List.hd l1) l2)) || not (not (subset l2 l3 && subset (List.tl l1) l2) || subset (List.tl l1) l3)) || not (subset l2 l3)) || not (subset l1 l2)) || subset l1 l3start[1.317s, "1.1"] ((((l1 = [] || not (List.mem (List.hd l1) l2)) || not (not (subset l2 l3 && subset (List.tl l1) l2) || subset (List.tl l1) l3)) || not (subset l2 l3)) || not (subset l1 l2)) || subset l1 l3simplify
into true
expansions [subset, subset, subset, List.mem]
rewrite_steps mem_subset
mem_subset
forward_chaining
subproof
((not (subset l2 l3) || not (subset l1 l2)) || List.mem (List.hd l1) l2 && not (l1 = [])) || subset l1 l3start[1.317s, "1.2"] ((not (subset l2 l3) || not (subset l1 l2)) || List.mem (List.hd l1) l2 && not (l1 = [])) || subset l1 l3
simplify
into ((subset l1 l3 || List.mem (List.hd l1) l2) || not (subset l1 l2)) || not (subset l2 l3)
expansions [subset, List.mem, List.mem]
rewrite_steps mem_subset
forward_chaining simplify
into true
expansions [subset, subset]
rewrite_steps forward_chaining
Loading..
This forward chaining rule will match only if a goal contains terms that match both subset l1 l2 and subset l1 l3.
It should be noted that Imandra supports automatic trigger selection, meaning it's often not necessary to annotate the trigger terms manually as Imandra can infer for us both simple triggers and trigger clusters, in fact for both the single trigger examples above, we could've omitted the trigger annotations and Imandra would've picked up exactly those terms as triggers.
Induction¶
While bounded solving and simplification can get us a long way towards formally verifying our software, neither technique is enough on its own when we need to exhaustively reason about properties over infinite state spaces, thankfully Imandra puts at our disposal a very powerful reasoning technique that can do just that: induction.
Induction is a proof technique that can be used to prove that some property P(x) holds for all the elements x of a recursively defined structure (e.g. integers, lists, etc) or, more generally, of any well ordered set. The proof consists of:
- a proof that
P(base)is true for each base case - a proof that if
P(x)is true (called the inductive hypothesis), thenP(step(x))is also true, for all the recursive steps of the property we're trying to prove
We call the set of base cases and step cases for a goal, its induction scheme.
Induction schemes can automatically be derived by Imandra using structural induction, from analysis over the recursively defined structures the goal applies to, or using functional induction (also called recursive induction), from analysis of the termination proof used to admit the recursive functions that appear in the goal we're trying to prove.
Concretely, examples of induction schemes are:
- for the natural numbers,
P(0) && P(x) ==> P(x+1), where0is the base case,P(x)is the inductive hypothesis andP(x+1)is the inductive step - for lists,
P([]) && (x <> [] && P(tail(x)) ==> P (x)), where[]is the base case,x <> [] && P(tail(x))is the inductive hypothesis andP(x)is the inductive step. - for the function
repeatas defined below,n <= 0 ==> P(n, c) && (n > 0 && P(n - 1, c)) ==> P(n, c)wheren <= 0 ==> P(n, c)is the base case,n > 0 && P(n - 1, c)is the inductive hypothesis andP(n, c)is the inductive step
In [28]:
let rec repeat c n =
if n <= 0 then
[]
else
c :: (repeat c (n-1))
Out[28]:
val repeat : 'a -> int -> 'a list = <fun>
termination proof
Termination proof
call `repeat c (n - 1)` from `repeat c n`
| original | repeat c n | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | repeat c (n - 1) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (if n >= 0 then n else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [not (n <= 0)] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
The first two examples are induction schemes derived by structural induction on the natural numbers and list datatypes, the last example is an instance derived by functional induction on repeat.
For any non-trivial goal there may be more than one valid induction scheme available, choosing the correct scheme to induct on can be a crucial step in order to be able to close the proof. Imandra has a powerful machinery for scoring, subsuming and merging induction schemes and will often do a very good of making the right decision, however, in case it doesn't, it is also possible to manually specify the induction scheme.
Let's use the following property to exemplify how we can affect the induction scheme used to prove it:
In [29]:
let phi lst =
List.for_all ((<) 0) lst ==>
List.fold_right (+) ~base:1 lst > 0
Out[29]:
val phi : int list -> bool = <fun>
We can see that if we let Imandra pick the induction scheme automatically, its heuristics will derive it from functional induction on List.for_all:
In [30]:
verify (fun lst -> phi lst) [@@induct]
Out[30]:
- : int list -> bool = <fun> Goal: phi lst. 1 nontautological subgoal. Subgoal 1: H0. List.for_all ((<) 0) lst H1. List.fold_right + 1 lst <= 0 |--------------------------------------------------------------------------- false Verified up to bound 10 (after 0.052s). Must try induction. The recursive terms in the conjecture suggest 2 inductions. Subsumption and merging reduces this to 1. We shall induct according to a scheme derived from List.for_all. Induction scheme: (lst = [] ==> φ lst) && (not (lst = []) && φ (List.tl lst) ==> φ lst). 2 nontautological subgoals. Subgoal 1.2: H0. lst = [] H1. List.for_all ((<) 0) lst H2. List.fold_right + 1 lst <= 0 |--------------------------------------------------------------------------- false But simplification reduces this to true, using the definitions of List.fold_right and List.for_all. Subgoal 1.1: H0. not (lst = []) H1. not (List.for_all ((<) 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0) H2. List.for_all ((<) 0) lst H3. List.fold_right + 1 lst <= 0 |--------------------------------------------------------------------------- false But simplification reduces this to true, using the definitions of List.fold_right and List.for_all.
Proved
proof
| ground_instances | 0 |
| definitions | 5 |
| inductions | 1 |
| search_time | 0.210s |
Expand
start[0.210s, "Goal"] List.for_all ((<) 0) :var_0: ==> List.fold_right + 1 :var_0: > 0
subproof
not (List.for_all ((<) 0) lst) || not (List.fold_right + 1 lst <= 0)start[0.210s, "1"] not (List.for_all ((<) 0) lst) || not (List.fold_right + 1 lst <= 0)
induction on (functional ) :scheme (lst = [] ==> φ lst) && (not (lst = []) && φ (List.tl lst) ==> φ lst)Split (((not (lst = []) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)) && ((not (not (lst = []) && (not (List.for_all ((<) 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)) :cases [(not (lst = []) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0); ((lst = [] || not (not (List.for_all ((<) 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)])subproof
((lst = [] || not (not (List.for_all ((<) 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)start[0.104s, "1.1"] ((lst = [] || not (not (List.for_all ((<) 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)simplify
into true
expansions [List.for_all, List.fold_right, List.for_all]
rewrite_steps forward_chaining
subproof
(not (lst = []) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)start[0.104s, "1.2"] (not (lst = []) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)
simplify
into true
expansions [List.fold_right, List.for_all]
rewrite_steps forward_chaining
Loading..
We can force imandra to use an induction scheme derived from structural induction on lst instead:
In [31]:
verify (fun lst -> phi lst) [@@induct structural lst]
Out[31]:
- : int list -> bool = <fun> Goal: phi lst. 1 nontautological subgoal. Subgoal 1: H0. List.for_all ((<) 0) lst H1. List.fold_right + 1 lst <= 0 |--------------------------------------------------------------------------- false Verified up to bound 10 (after 0.053s). Must try induction. Induction scheme: φ [] && (lst <> [] && φ (List.tl lst) ==> φ lst). 2 nontautological subgoals. Subgoal 1.2: H0. List.for_all ((<) 0) [] H1. List.fold_right + 1 [] <= 0 |--------------------------------------------------------------------------- false But simplification reduces this to true, using the definitions of List.fold_right and List.for_all. Subgoal 1.1: H0. lst <> [] H1. not (List.for_all ((<) 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0) H2. List.for_all ((<) 0) lst H3. List.fold_right + 1 lst <= 0 |--------------------------------------------------------------------------- false But simplification reduces this to true, using the definitions of List.fold_right and List.for_all.
Proved
proof
| ground_instances | 0 |
| definitions | 5 |
| inductions | 1 |
| search_time | 0.215s |
Expand
start[0.215s, "Goal"] List.for_all ((<) 0) :var_0: ==> List.fold_right + 1 :var_0: > 0
subproof
not (List.for_all ((<) 0) lst) || not (List.fold_right + 1 lst <= 0)start[0.215s, "1"] not (List.for_all ((<) 0) lst) || not (List.fold_right + 1 lst <= 0)
induction on (structural+ lst) :scheme φ [] && (lst <> [] && φ (List.tl lst) ==> φ lst)
Split ((not (List.for_all ((<) 0) []) || not (List.fold_right + 1 [] <= 0)) && ((not (lst <> [] && (not (List.for_all ((<) 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)) :cases [not (List.for_all ((<) 0) []) || not (List.fold_right + 1 [] <= 0); ((not (lst <> []) || not (not (List.for_all ((<) 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)])subproof
((not (lst <> []) || not (not (List.for_all ((<) 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)start[0.110s, "1.1"] ((not (lst <> []) || not (not (List.for_all ((<) 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)simplify
into true
expansions [List.for_all, List.fold_right, List.for_all]
rewrite_steps forward_chaining
subproof
not (List.for_all ((<) 0) []) || not (List.fold_right + 1 [] <= 0)start[0.110s, "1.2"] not (List.for_all ((<) 0) []) || not (List.fold_right + 1 [] <= 0)
simplify
into true
expansions [List.fold_right, List.for_all]
rewrite_steps forward_chaining
Loading..
Comparing the two induction schemes, we can see that they are equivalent as List.for_all does a simple structural recursion.
In order to manually specify a functional induction, one must use a recursive function encoding the recursion scheme we want to induct over (Imandra doesn't care what the function does, it only looks at its recursion scheme, so when we need to synthesize a function to suggest an induction scheme we usually make it return a boolean).
In [32]:
let rec induct_scheme (lst : int list) =
match lst with
| [] -> true
| (_::tail) -> induct_scheme tail;;
Out[32]:
val induct_scheme : int list -> bool = <fun>
termination proof
Termination proof
call `induct_scheme (List.tl lst)` from `induct_scheme lst`
| original | induct_scheme lst | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | induct_scheme (List.tl lst) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (Ordinal.count lst) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (Ordinal.count (List.tl lst)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [not (lst = [])] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
In [33]:
verify (fun lst -> phi lst) [@@induct functional induct_scheme]
Out[33]:
- : int list -> bool = <fun> Goal: phi lst. 1 nontautological subgoal. Subgoal 1: H0. List.for_all ((<) 0) lst H1. List.fold_right + 1 lst <= 0 |--------------------------------------------------------------------------- false Verified up to bound 10 (after 0.053s). Must try induction. Note: We must proceed by induction, but our current subgoal is less appropriate for induction than our original conjecture. Thus, we prefer to abandon our work until now and return our focus to the original conjecture which we shall attempt to prove by induction directly. Experimental: You are using new support for non-present functional inductions! Induction scheme: (lst = [] ==> φ lst) && (not (lst = []) && φ (List.tl lst) ==> φ lst). 2 nontautological subgoals. Subgoal 2: H0. lst = [] H1. List.for_all ((<) 0) lst H2. List.fold_right + 1 lst <= 0 |--------------------------------------------------------------------------- false But simplification reduces this to true, using the definitions of List.fold_right and List.for_all. Subgoal 1: H0. not (lst = []) H1. not (List.for_all ((<) 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0) H2. List.for_all ((<) 0) lst H3. List.fold_right + 1 lst <= 0 |--------------------------------------------------------------------------- false But simplification reduces this to true, using the definitions of List.fold_right and List.for_all.
Proved
proof
| ground_instances | 0 |
| definitions | 5 |
| inductions | 1 |
| search_time | 0.212s |
Expand
start[0.212s, "Goal"] List.for_all ((<) 0) :var_0: ==> List.fold_right + 1 :var_0: > 0
subproof
not (List.for_all ((<) 0) lst) || not (List.fold_right + 1 lst <= 0)start[0.212s, "1"] not (List.for_all ((<) 0) lst) || not (List.fold_right + 1 lst <= 0)
induction on (functional induct_scheme) :scheme (lst = [] ==> φ lst) && (not (lst = []) && φ (List.tl lst) ==> φ lst)Split (((not (lst = []) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)) && ((not (not (lst = []) && (not (List.for_all ((<) 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)) :cases [(not (lst = []) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0); ((lst = [] || not (not (List.for_all ((<) 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)])subproof
((lst = [] || not (not (List.for_all ((<) 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)start[0.104s, "1"] ((lst = [] || not (not (List.for_all ((<) 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)simplify
into true
expansions [List.for_all, List.fold_right, List.for_all]
rewrite_steps forward_chaining
subproof
(not (lst = []) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)start[0.104s, "2"] (not (lst = []) || not (List.for_all ((<) 0) lst)) || not (List.fold_right + 1 lst <= 0)
simplify
into true
expansions [List.fold_right, List.for_all]
rewrite_steps forward_chaining
Loading..
Note that it's quite rare to have to encode manually the induction scheme like that, most of the times you'll need to instruct Imandra to use a different scheme than the one it automatically picked, you'll simply need to use the "key recursive function" in your goal, for example in our phi, we'd pick List.fold_right
The final distinction we need to make is between the additive and multiplicative flavor of structural induction (when we talk about structural induction without specifying the flavor, we usually mean additive, as that's the default structural mode Imandra uses).
The distinction between the two flavor only manifests when one is inducting over more tha one structure and it affects the way base cases and inductive steps are mixed, let's assume one needs to do induction on x, y:
addictive structural induction gives you 3 cases: two base cases
P(x_base, y),P(x, y_base)and one inductive stepP(x,y) ==> P(step(x), step(y))multiplicative structural induction gives you 4 cases: one base case
P(x_base, y_base)and three inductive stepsP(x, y_base) ==> P(step(x), y_base),P(x_base, y) ==> P(x_base, step(y))andP(x,y) ==> P(step(x), step(y))
Practically, we can see the difference using the following function:
In [34]:
let rec interleave_strict x y = match x, y with
| [], _ | _ , [] -> []
| x::xs, y::ys -> x::y::(interleave_strict xs ys)
Out[34]:
val interleave_strict : 'a list -> 'a list -> 'a list = <fun>
termination proof
Termination proof
call `interleave_strict (List.tl x) (List.tl y)` from `interleave_strict x y`
| original | interleave_strict x y | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub | interleave_strict (List.tl x) (List.tl y) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original ordinal | Ordinal.Int (Ordinal.count x) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| sub ordinal | Ordinal.Int (Ordinal.count (List.tl x)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| path | [not (x = [] || y = [])] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| proof | detailed proof
Expand
|
Let's prove that the length of interleave_strict x y is always less than or equal to the total length of x and y summed, first using additive and then using multiplicative structural induction:
In [35]:
verify (fun x y ->
List.length @@ interleave_strict x y <= List.length x + List.length y)
[@@induct structural_add (x,y)]
Out[35]:
- : 'a list -> 'a list -> bool = <fun> Goal: (List.length @@ interleave_strict x y) <= (List.length x + List.length y). 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- List.length (interleave_strict x y) <= (List.length x + List.length y) Verified up to bound 10 (after 0.054s). Must try induction. Induction scheme: φ y [] && φ [] x && (x <> [] && y <> [] && φ (List.tl y) (List.tl x) ==> φ y x). 3 nontautological subgoals. Subgoal 1.3: |--------------------------------------------------------------------------- List.length (interleave_strict [] y) <= (List.length [] + List.length y) But simplification reduces this to true, using the definitions of List.length and interleave_strict. Subgoal 1.2: |--------------------------------------------------------------------------- List.length (interleave_strict x []) <= (List.length x + List.length []) But simplification reduces this to true, using the definitions of List.length and interleave_strict. Subgoal 1.1: H0. x <> [] H1. y <> [] H2. List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)) |--------------------------------------------------------------------------- List.length (interleave_strict x y) <= (List.length x + List.length y) This simplifies, using the definitions of List.length and interleave_strict to: Subgoal 1.1': H0. List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)) H1. y <> [] H2. x <> [] |--------------------------------------------------------------------------- List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y))) <= ((1 + List.length (List.tl x)) + List.length (List.tl y)) But simplification reduces this to true, using the definition of List.length.
Proved
proof
| ground_instances | 0 |
| definitions | 11 |
| inductions | 1 |
| search_time | 0.451s |
Expand
start[0.451s, "Goal"] List.length (interleave_strict :var_0: :var_1:) <= (List.length :var_0: + List.length :var_1:)
subproof
List.length (interleave_strict x y) <= (List.length x + List.length y)start[0.450s, "1"] List.length (interleave_strict x y) <= (List.length x + List.length y)
induction on (structural+ x, y) :scheme φ y [] && φ [] x && (x <> [] && y <> [] && φ (List.tl y) (List.tl x) ==> φ y x)Split ((List.length (interleave_strict [] y) <= (List.length [] + List.length y) && List.length (interleave_strict x []) <= (List.length x + List.length [])) && (not ((x <> [] && y <> []) && List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y))) || List.length (interleave_strict x y) <= (List.length x + List.length y)) :cases [List.length (interleave_strict [] y) <= (List.length [] + List.length y); List.length (interleave_strict x []) <= (List.length x + List.length []); ((not (x <> []) || not (y <> [])) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || List.length (interleave_strict x y) <= (List.length x + List.length y)])subproof
((not (x <> []) || not (y <> [])) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || List.length (interleave_strict x y) <= (List.length x + List.length y)start[0.345s, "1.1"] ((not (x <> []) || not (y <> [])) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || List.length (interleave_strict x y) <= (List.length x + List.length y)simplify
into ((List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y))) <= ((1 + List.length (List.tl x)) + List.length (List.tl y)) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || not (y <> [])) || not (x <> [])expansions [List.length, List.length, List.length, interleave_strict]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
simplify
into true
expansions List.length
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
subproof
List.length (interleave_strict x []) <= (List.length x + List.length [])start[0.345s, "1.2"] List.length (interleave_strict x []) <= (List.length x + List.length [])
simplify
into true
expansions [List.length, List.length, interleave_strict]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
subproof
List.length (interleave_strict [] y) <= (List.length [] + List.length y)start[0.345s, "1.3"] List.length (interleave_strict [] y) <= (List.length [] + List.length y)
simplify
into true
expansions [List.length, List.length, interleave_strict]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
Loading..
In [36]:
verify (fun x y ->
List.length @@ interleave_strict x y <= List.length x + List.length y)
[@@induct structural_mult (x,y)]
Out[36]:
- : 'a list -> 'a list -> bool = <fun> Goal: (List.length @@ interleave_strict x y) <= (List.length x + List.length y). 1 nontautological subgoal. Subgoal 1: |--------------------------------------------------------------------------- List.length (interleave_strict x y) <= (List.length x + List.length y) Verified up to bound 10 (after 0.054s). Must try induction. Induction scheme: φ [] [] && (x <> [] && φ [] (List.tl x) ==> φ [] x) && (y <> [] && φ (List.tl y) [] ==> φ y []) && (x <> [] && y <> [] && φ (List.tl y) (List.tl x) ==> φ y x). 4 nontautological subgoals. Subgoal 1.4: |--------------------------------------------------------------------------- List.length (interleave_strict [] []) <= (2 * List.length []) But simplification reduces this to true, using the definitions of List.length and interleave_strict. Subgoal 1.3: H0. x <> [] H1. List.length (interleave_strict (List.tl x) []) <= (List.length (List.tl x) + List.length []) |--------------------------------------------------------------------------- List.length (interleave_strict x []) <= (List.length x + List.length []) But simplification reduces this to true, using the definitions of List.length and interleave_strict. Subgoal 1.2: H0. y <> [] H1. List.length (interleave_strict [] (List.tl y)) <= (List.length [] + List.length (List.tl y)) |--------------------------------------------------------------------------- List.length (interleave_strict [] y) <= (List.length [] + List.length y) But simplification reduces this to true, using the definitions of List.length and interleave_strict. Subgoal 1.1: H0. x <> [] H1. y <> [] H2. List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)) |--------------------------------------------------------------------------- List.length (interleave_strict x y) <= (List.length x + List.length y) This simplifies, using the definitions of List.length and interleave_strict to: Subgoal 1.1': H0. List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)) H1. y <> [] H2. x <> [] |--------------------------------------------------------------------------- List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y))) <= ((1 + List.length (List.tl x)) + List.length (List.tl y)) But simplification reduces this to true, using the definition of List.length.
Proved
proof
| ground_instances | 0 |
| definitions | 22 |
| inductions | 1 |
| search_time | 0.526s |
Expand
start[0.526s, "Goal"] List.length (interleave_strict :var_0: :var_1:) <= (List.length :var_0: + List.length :var_1:)
subproof
List.length (interleave_strict x y) <= (List.length x + List.length y)start[0.526s, "1"] List.length (interleave_strict x y) <= (List.length x + List.length y)
induction on (structural* x, y) :scheme φ [] [] && (x <> [] && φ [] (List.tl x) ==> φ [] x) && (y <> [] && φ (List.tl y) [] ==> φ y []) && (x <> [] && y <> [] && φ (List.tl y) (List.tl x) ==> φ y x)Split (((List.length (interleave_strict [] []) <= (2 * List.length []) && (not (x <> [] && List.length (interleave_strict (List.tl x) []) <= (List.length (List.tl x) + List.length [])) || List.length (interleave_strict x []) <= (List.length x + List.length []))) && (not (y <> [] && List.length (interleave_strict [] (List.tl y)) <= (List.length [] + List.length (List.tl y))) || List.length (interleave_strict [] y) <= (List.length [] + List.length y))) && (not ((x <> [] && y <> []) && List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y))) || List.length … <= …) :cases [List.length (interleave_strict [] []) <= (2 * List.length []); (not (x <> []) || not (List.length (interleave_strict (List.tl x) []) <= (List.length (List.tl x) + List.length []))) || List.length (interleave_strict x []) <= (List.length x + List.length []); (not (y <> []) || not (List.length (interleave_strict [] (List.tl y)) <= (List.length [] + List.length (List.tl y)))) || List.length (interleave_strict [] y) <= (List.length [] + List.length y); ((not (x <> []) || not (y <> [])) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || List.length (interleave_strict x y) <= (List.length x + List.length y)])subproof
((not (x <> []) || not (y <> [])) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || List.length (interleave_strict x y) <= (List.length x + List.length y)start[0.415s, "1.1"] ((not (x <> []) || not (y <> [])) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || List.length (interleave_strict x y) <= (List.length x + List.length y)simplify
into ((List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y))) <= ((1 + List.length (List.tl x)) + List.length (List.tl y)) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || not (y <> [])) || not (x <> [])expansions [List.length, List.length, List.length, interleave_strict]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
simplify
into true
expansions List.length
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
subproof
(not (y <> []) || not (List.length (interleave_strict [] (List.tl y)) <= (List.length [] + List.length (List.tl y)))) || List.length (interleave_strict [] y) <= (List.length [] + List.length y)start[0.415s, "1.2"] (not (y <> []) || not (List.length (interleave_strict [] (List.tl y)) <= (List.length [] + List.length (List.tl y)))) || List.length (interleave_strict [] y) <= (List.length [] + List.length y)simplify
into true
expansions [List.length, List.length, List.length, interleave_strict, List.length, List.length, interleave_strict]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
subproof
(not (x <> []) || not (List.length (interleave_strict (List.tl x) []) <= (List.length (List.tl x) + List.length []))) || List.length (interleave_strict x []) <= (List.length x + List.length [])start[0.415s, "1.3"] (not (x <> []) || not (List.length (interleave_strict (List.tl x) []) <= (List.length (List.tl x) + List.length []))) || List.length (interleave_strict x []) <= (List.length x + List.length [])simplify
into true
expansions [List.length, List.length, List.length, interleave_strict, List.length, List.length, interleave_strict]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
subproof
List.length (interleave_strict [] []) <= (2 * List.length [])start[0.415s, "1.4"] List.length (interleave_strict [] []) <= (2 * List.length [])
simplify
into true
expansions [List.length, List.length, interleave_strict]
rewrite_steps forward_chaining List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
List.len_nonnegative
List.len_nonnegative
len_non_neg
len_non_neg
len_nonnegative
len_nonnegative
rev_len_fc
rev_len_fc
Loading..
Imandra was able to prove the property using both flavors of structural induction, but we can see that the proof using the additive flavor was shorter. The multiplicative flavor will almost always result in longer proofs than the additive flavorm, it should be easy to understand why that is, as the number of cases produced by the additive flavor is linear on the number of structures while the multiplicative one is combinatorial.